;  <origin>BepiColombo_Models_V3.3 | csw_C0 | thm2/THM</origin>
;  <theories>
;    <theory name="basic_set"/>
;  </theories>
;  <typenv>
;    <variable name="S" type="POW(S)"/>
;    <variable name="a" type="S"/>
;    <variable name="b" type="S"/>
;    <variable name="c" type="S"/>
;  </typenv>
;  <hypothesis>� a=b</hypothesis>
;  <hypothesis>� b=c</hypothesis>
;  <hypothesis>� c=a</hypothesis>
;  <hypothesis>S={a,b,c}</hypothesis>
;  <goal>{a,b,c} = {c,a,b}</goal>
; </lemma>
(benchmark bepi_colombo_thm2
  :logic AUFLIA
  :extrasorts (S)
  :extrafuns ((a S) (b S) (c S))
  :extramacros (
  		 (enum1 
		  (lambda (?elem S) . 
		    (or (= ?elem a) (= ?elem b) (= ?elem c))))
		 (enum2 
		   (lambda (?elem S) . 
		     (or (= ?elem c) (= ?elem a) (= ?elem b))))
		 )
  :assumption (distinct a b c)
  :assumption (forall (?elem S) 
		(or 
		  (= ?elem a)
		  (= ?elem b)
		  (= ?elem c)))
  
  :formula
  (not
      (= enum1 enum2)
    )
)
    